Nuprl Lemma : list_accum_append
11,40
postcript
pdf
A
,
B
:(top List),
y
,
f
:top.
sqequal(list_accum(
x
,
a
.
f
(
x
,
a
);
y
; append(
A
;
B
));
sqequal(
list_accum(
x
,
a
.
f
(
x
,
a
); list_accum(
x
,
a
.
f
(
x
,
a
);
y
;
A
);
B
))
latex
Definitions
x
:
A
.
B
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
top
,
t
T
Lemmas
top
wf
origin
A,B:(top List), y,f:top.
A,B:(top List), y,f:top.
x:A. B(x)
x,y. t(x;y)
T